#if !defined(ProverHeader)
#define ProverHeader

#include <map>

class ProverFactoryBase;
class Rules;
class Snippet;
class System;

#include "bind.h"
#include "node.h"
#include "prototype.h"
#include "tuple.h"

// A coroutine holder, a template for predicates prover
class Prover {
public:

  // Let me call this a polymorphized constructor
  static Prover *create (Node&, System&);

  virtual ~Prover () {
  }

  virtual bool prove () = 0;

  // Setup routine, choose one (not constructor)
  virtual void set (Atom&, System&) {
  }
  virtual void set (Tuple&, System&) {
  }
  virtual void set (Tree&, System&) {
  }

  // Process built-in routines, or fail if not
  static ProverFactoryBase *findSystemPredicate (const Prototype&);
  static Prover *createSystemPredicate (ProverFactoryBase*, Node&, System&);

  static Snippet *getSnippet (Prototype&, Node&, System&);

  // To extract the "remaining tuple" to deal with in assert/not etc.
  pNode excludeFirst (Tuple &tuple) {
    int size = tuple.nodes.size ();

    if(size < 2)
      return Atom::create ("");
    else if(size == 2)
      return tuple.nodes[1];
    else {
      Tuple *toAssert = new Tuple;
      toAssert->nodes.insert (toAssert->nodes.begin (), tuple.nodes.begin ()
          + 1, tuple.nodes.end ());
      return toAssert;
    }
  }

  typedef std::multimap<Prototype, ProverFactoryBase*> ProversMap;
  static ProversMap *proversMap;
  static ProversMap *varArgsProversMap; // Variable no of arguments, like write
};

// Predicates that can only be proved once
class OnceProver : public Prover {
public:
  OnceProver () :
    proved (false) {
  }
  virtual ~OnceProver () {
  }
  virtual bool prove ();
  virtual bool proveOnce () = 0;

  bool proved;
};

class OnceBindProver : public OnceProver {
public:
  virtual ~OnceBindProver () {
  }
  virtual bool prove ();
  void set (System &s) {
    system = &s;
  }

  Binder binder;
  System *system;
};

class OnceBindTupleProver : public OnceBindProver {
public:
  virtual ~OnceBindTupleProver () {
  }
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }

  Tuple *tuple;
};

#define predicateName(s) public: static const char *name () { return s; }

#endif
